Termination of Nested and Mutually Recursive Algorithms
Identifieur interne : 00BC08 ( Main/Exploration ); précédent : 00BC07; suivant : 00BC09Termination of Nested and Mutually Recursive Algorithms
Auteurs : Jürgen Giesl [Allemagne]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1997-08-01.
English descriptors
Abstract
Abstract: This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion. We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthy’s f_91 function).
Url:
DOI: 10.1023/A:1005797629953
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001C38
- to stream Istex, to step Curation: 001C17
- to stream Istex, to step Checkpoint: 002741
- to stream Main, to step Merge: 00C386
- to stream Main, to step Curation: 00BC08
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Termination of Nested and Mutually Recursive Algorithms</title><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:7A799CE5F9D1C230ABF22435238DDB01A3FB77F3</idno><date when="1997" year="1997">1997</date><idno type="doi">10.1023/A:1005797629953</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-15T118FD-L/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001C38</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001C38</idno><idno type="wicri:Area/Istex/Curation">001C17</idno><idno type="wicri:Area/Istex/Checkpoint">002741</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002741</idno><idno type="wicri:doubleKey">0168-7433:1997:Giesl J:termination:of:nested</idno><idno type="wicri:Area/Main/Merge">00C386</idno><idno type="wicri:Area/Main/Curation">00BC08</idno><idno type="wicri:Area/Main/Exploration">00BC08</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Termination of Nested and Mutually Recursive Algorithms</title><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>FB Informatik, TH Darmstadt, Alexanderstr. 10, 64283, Darmstadt</wicri:regionArea><placeName><region type="land" nuts="1">Hesse (Land)</region><region type="district" nuts="2">District de Darmstadt</region><settlement type="city">Darmstadt</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="1997-08-01">1997-08-01</date><biblScope unit="volume">19</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="29">29</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automated termination analysis</term><term>functional programming</term><term>induction theorem proving</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion. We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthy’s f_91 function).</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>District de Darmstadt</li><li>Hesse (Land)</li></region><settlement><li>Darmstadt</li></settlement></list><tree><country name="Allemagne"><region name="Hesse (Land)"><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></region><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00BC08 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00BC08 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:7A799CE5F9D1C230ABF22435238DDB01A3FB77F3
|texte= Termination of Nested and Mutually Recursive Algorithms
}}
| This area was generated with Dilib version V0.6.33. |  |